\chapter{Appendix}
\label{appendix}
\section{SIMPLE}
The following definition is the semantics of SIMPLE \cite{kpage} language.
 \vspace*{3ex}
 % end latex header 
 \begin{module}{\moduleName{SIMPLE-UNTYPED-SYNTAX}}
 \including{\moduleName{K-LATEX}\modulePlus{}\moduleName{PL-ID}\modulePlus{}\moduleName{PL-INT}}
 \sorts{\sort{Decl}\sort{Exp}\sort{List\{Exp\}}\sort{List\{Id\}}\sort{Stmt}\sort{Stmts}}
 \begin{latexComment}
  \subsection{Identifiers}
 The special identifier for the function ``main'' belongs to all programs.
 Each program may use additional identifiers, which need to be declared either
 automatically (when one uses an external parser) or manually (when one writes the program). 
 \end{latexComment}
 \syntax{\nonTerminal{\sort{Id}}}{\terminal{main}}{}
 \begin{latexComment}
  \subsection{Declarations}
 There are two types of declarations: for variables (including arrays) and for functions.
 As our current parser is ``algebraic'', the empty list needs to be identifiable as a constant
 (unlike CFG grammars, where it can simply be the empty string/epsilon production).  Therefore,
 if only using the first syntactic production for function declarations, one would need to
 explicitly specify the empty list constant for declaring a function with zero arguments.
 To avoid having to do that, we add a separate function declaration production with explicitly
 no arguments; this is desugared into the first one. 
 \end{latexComment}
 \syntax{\nonTerminal{\sort{Decl}}}{\terminal{function}{\nonTerminal{\sort{Id}}}\terminal{(}{\nonTerminal{\sort{List\{Id\}}}}\terminal{)}{\nonTerminal{\sort{Stmt}}}}{}
 \syntaxCont{\nonTerminal{\sort{Decl}}}{\terminal{var}{\nonTerminal{\sort{List\{Exp\}}}}\terminal{;}}{}
 \syntaxCont{\nonTerminal{\sort{Decl}}}{\terminal{function}{\nonTerminal{\sort{Id}}}\terminal{()}{\nonTerminal{\sort{Stmt}}}}{}
 \begin{latexComment}
  \subsection{Expressions}
 The expression constructs below are standard.  Increment (\texttt{++}) takes an
 expression rather than a variable because it can also increment an array element.
 Arrays can be multidimensional and can hold other arrays, so their lookup operation
 takes a list of expressions as argument and applies to an expression (which can
 in particular be another array lookup), respectively.
 The construct \texttt{sizeof} gives the size of an array in number of elements of
 its first dimension.
 Like for the declaration of functions above, we have separate syntax for function
 calls with zero arguments.
 Note that almost all constructs are strict.  Exceptions are the increment (since
 its first argument gets updated, so it cannot be evaluated), the function call
 with zero arguments (because it will get desugared), and the assignment which
 is only strict in its second argument (for the same reason as the increment). 
 \end{latexComment}
 \syntax{\nonTerminal{\sort{Exp}}}{\terminal{++}{\nonTerminal{\sort{Exp}}}}{}
 \syntaxCont{\nonTerminal{\sort{Exp}}}{\crlbracket{\nonTerminal{\sort{Bool}}}}{}
 \syntaxCont{\nonTerminal{\sort{Exp}}}{\crlbracket{\nonTerminal{\sort{Id}}}}{}
 \syntaxCont{\nonTerminal{\sort{Exp}}}{\crlbracket{\nonTerminal{\sort{Int}}}}{}
 \syntaxCont{\nonTerminal{\sort{Exp}}}{{\nonTerminal{\sort{Exp}}}\terminal{+}{\nonTerminal{\sort{Exp}}}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Exp}}}{{\nonTerminal{\sort{Exp}}}\terminal{-}{\nonTerminal{\sort{Exp}}}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Exp}}}{{\nonTerminal{\sort{Exp}}}\terminal{*}{\nonTerminal{\sort{Exp}}}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Exp}}}{{\nonTerminal{\sort{Exp}}}\terminal{/}{\nonTerminal{\sort{Exp}}}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Exp}}}{{\nonTerminal{\sort{Exp}}}\terminal{\%}{\nonTerminal{\sort{Exp}}}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Exp}}}{\terminal{-}{\nonTerminal{\sort{Exp}}}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Exp}}}{{\nonTerminal{\sort{Exp}}}\terminal{<}{\nonTerminal{\sort{Exp}}}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Exp}}}{{\nonTerminal{\sort{Exp}}}\terminal{<=}{\nonTerminal{\sort{Exp}}}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Exp}}}{{\nonTerminal{\sort{Exp}}}\terminal{>}{\nonTerminal{\sort{Exp}}}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Exp}}}{{\nonTerminal{\sort{Exp}}}\terminal{>=}{\nonTerminal{\sort{Exp}}}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Exp}}}{{\nonTerminal{\sort{Exp}}}\terminal{==}{\nonTerminal{\sort{Exp}}}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Exp}}}{{\nonTerminal{\sort{Exp}}}\terminal{!=}{\nonTerminal{\sort{Exp}}}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Exp}}}{{\nonTerminal{\sort{Exp}}}\terminal{and}{\nonTerminal{\sort{Exp}}}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Exp}}}{{\nonTerminal{\sort{Exp}}}\terminal{or}{\nonTerminal{\sort{Exp}}}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Exp}}}{\terminal{not}{\nonTerminal{\sort{Exp}}}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Exp}}}{{\nonTerminal{\sort{Exp}}}\terminal{[}{\nonTerminal{\sort{List\{Exp\}}}}\terminal{]}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Exp}}}{\terminal{sizeOf(}{\nonTerminal{\sort{Exp}}}\terminal{)}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Exp}}}{{\nonTerminal{\sort{Exp}}}\terminal{()}}{}
 \syntaxCont{\nonTerminal{\sort{Exp}}}{{\nonTerminal{\sort{Exp}}}\terminal{(}{\nonTerminal{\sort{List\{Exp\}}}}\terminal{)}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Exp}}}{\terminal{read()}}{}
 \syntaxCont{\nonTerminal{\sort{Exp}}}{{\nonTerminal{\sort{Exp}}}\terminal{=}{\nonTerminal{\sort{Exp}}}}{\kstrict{2}{}}
 \begin{latexComment}
  \subsection{Statements}
 Most of the statement constructs are standard for imperative languages.
 We also syntactically distinguish between empty and non-empty blocks.
 Variables can be declared anywhere inside a block, their scope ending
 with the block.
 Expressions are allowed to be used for their side-effects only (followed
 by a semicolon ``\texttt{;}'').
 Functions are allowed to abruptly return.
 The exceptions are parametric, i.e., one can throw a value which is bound
 to the variable declared by \texttt{catch}.
 Threads can be dynamically created and terminated, and can synchronize with
 \texttt{acquire}, \texttt{release} and \texttt{rendezvous}.
 Note that the strictness attributes obey the intended evaluation strategy
 of the various constructs.  In particular, the if-then-else construct is
 strict only in its first argument (the if-then construct will be desugared
 into if-then-else), while the loops constructs are not strict in any
 arguments. 
 \end{latexComment}
 \syntax{\nonTerminal{\sort{Stmt}}}{\terminal{\{}{\nonTerminal{\sort{Stmts}}}\terminal{\}}}{}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{\terminal{\{\}}}{}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{{\nonTerminal{\sort{Exp}}}\terminal{;}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{\terminal{if}{\nonTerminal{\sort{Exp}}}\terminal{then}{\nonTerminal{\sort{Stmt}}}\terminal{else}{\nonTerminal{\sort{Stmt}}}}{\kstrict{1}{}}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{\terminal{if}{\nonTerminal{\sort{Exp}}}\terminal{then}{\nonTerminal{\sort{Stmt}}}}{}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{\terminal{while}{\nonTerminal{\sort{Exp}}}\terminal{do}{\nonTerminal{\sort{Stmt}}}}{}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{\terminal{for}{\nonTerminal{\sort{Id}}}\terminal{=}{\nonTerminal{\sort{Exp}}}\terminal{to}{\nonTerminal{\sort{Exp}}}\terminal{do}{\nonTerminal{\sort{Stmt}}}}{}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{\terminal{return}{\nonTerminal{\sort{Exp}}}\terminal{;}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{\terminal{write(}{\nonTerminal{\sort{Exp}}}\terminal{);}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{\terminal{try}{\nonTerminal{\sort{Stmt}}}\terminal{catch(}{\nonTerminal{\sort{Id}}}\terminal{)}{\nonTerminal{\sort{Stmt}}}}{}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{\terminal{throw}{\nonTerminal{\sort{Exp}}}\terminal{;}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{\terminal{spawn}{\nonTerminal{\sort{Stmt}}}}{}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{\terminal{acquire}{\nonTerminal{\sort{Exp}}}\terminal{;}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{\terminal{release}{\nonTerminal{\sort{Exp}}}\terminal{;}}{\kstrict{}{}}
 \syntaxCont{\nonTerminal{\sort{Stmt}}}{\terminal{rendezvous}{\nonTerminal{\sort{Exp}}}\terminal{;}}{\kstrict{}{}}
 \syntax{\nonTerminal{\sort{Stmts}}}{{\nonTerminal{\sort{Stmts}}}\mathrel{}{\nonTerminal{\sort{Stmts}}}}{}
 \syntaxCont{\nonTerminal{\sort{Stmts}}}{\crlbracket{\nonTerminal{\sort{Decl}}}}{}
 \syntaxCont{\nonTerminal{\sort{Stmts}}}{\crlbracket{\nonTerminal{\sort{Stmt}}}}{}
 \begin{latexComment}
  \subsubsection{Lists}
 Currently we have to explicitly declare the syntactic lists
 (they will be eventually builtin).
 Note that they are associative, strict and hybrid, which means that once they
 reach the top of the computation each of their elements is evaluated to a result
 and the obtained list of results is automatically considered to be a result.
 We prefer to tag their units with the corresponding sort to avoid confusion. 
 \end{latexComment}
 \syntax{\nonTerminal{\sort{List\{Id\}}}}{\dotCt{List\{Id\}}}{}
 \syntaxCont{\nonTerminal{\sort{List\{Id\}}}}{\crlbracket{\nonTerminal{\sort{Id}}}}{}
 %\syntaxCont{\nonTerminal{\sort{List\{Id\}}}}{{\nonTerminal{\sort{List\{Id\}}}}\terminal{,}{\nonTerminal{\sort{List\{Id\}}}}}{\kassoc{} \khybrid{} \kid{\constant{\ensuremath{\dotCt{List\{Id\}}}}{List\{Id\}}} \kstrict{}{}}
 \syntax{\nonTerminal{\sort{List\{Exp\}}}}{\crlbracket{\nonTerminal{\sort{Exp}}}}{}
 \syntaxCont{\nonTerminal{\sort{List\{Exp\}}}}{\crlbracket{\nonTerminal{\sort{List\{Id\}}}}}{}
 \syntaxCont{\nonTerminal{\sort{List\{Exp\}}}}{{\nonTerminal{\sort{List\{Exp\}}}}\terminal{,}{\nonTerminal{\sort{List\{Exp\}}}}}{\kditto{}}
 \end{module}
The next module desugars some of SIMPLE's language constructs into core ones.
 We only want to give semantics to core constructs, so we get rid of the
 derived ones before we start the semantics.
 All desugaring macros below are straightforward.  For the semantics, we can therefore assume
 that all functions take a list of arguments, that each conditional has both
 branches, that there are only \texttt{while} loops, and that each variable is
 declared alone and is initialized. \\
 \begin{module}{\moduleName{SIMPLE-UNTYPED-DESUGARED-SYNTAX}}
 \including{\moduleName{K-LATEX}}
 \including{\moduleName{SIMPLE-UNTYPED-SYNTAX}}\\
 \mequation{}{{\terminal{if}{\variable{E}{Exp}}\terminal{then}{\variable{S}{Stmt}}}}{{\terminal{if}{\variable{E}{Exp}}\terminal{then}{\variable{S}{Stmt}}\terminal{else}{\constant{\ensuremath{\terminal{\{\}}}}{Stmt}}}}
 \mequation{}{\terminal{for}{\variable{X}{Id}}\terminal{=}{\variable{\ensuremath{{E}_{1}}}{Exp}}\terminal{to}{\variable{\ensuremath{{E}_{2}}}{Exp}}\terminal{do}{\variable{S}{Stmt}}}
 {\begin{array}[t]{l} \terminal{\{} {{\terminal{var}{\variable{X}{Id}}\terminal{;}}}\mathrel{}{{{{{\variable{X}{Id}}\terminal{=}{\variable{\ensuremath{{E}_{1}}}{Exp}}}}\terminal{;}}}\kBR {\begin{array}[t]{l} \terminal{while}{{{\variable{X}{Id}}\terminal{<=}{\variable{\ensuremath{{E}_{2}}}{Exp}}}}\terminal{do} \kBR  \terminal{\{}{{{\variable{S}{Stmt}}\mathrel{}{{{{{\variable{X}{Id}}\terminal{=}{{{\variable{X}{Id}}\terminal{+}{\constant{1}{Nat}}}}}}\terminal{;}}}}}\terminal{\}} \end{array}} \kBR \terminal{\}}\end{array}}
 \mequation{}{{\terminal{function}{\variable{F}{Id}}\terminal{()}{\variable{S}{Stmt}}}}{{\terminal{function}{\variable{F}{Id}}\terminal{(}{\constant{\ensuremath{\dotCt{List\{Id\}}}}{List\{Id\}}}\terminal{)}{\variable{S}{Stmt}}}}
 \mequation{}{{{\variable{E}{Exp}}\terminal{()}}}{{{\variable{E}{Exp}}\terminal{(}{\constant{\ensuremath{\dotCt{List\{Id\}}}}{List\{Id\}}}\terminal{)}}}
 \mequation{}{{\terminal{var}{{{{{\variable{E}{Exp}}\terminal{,}{\variable{\ensuremath{E '}}{Exp}}}}\terminal{,}{\variable{El}{List\{Exp\}}}}}\terminal{;}}}{{{{\terminal{var}{\variable{E}{Exp}}\terminal{;}}}\mathrel{}{{\terminal{var}{{{\variable{\ensuremath{E '}}{Exp}}\terminal{,}{\variable{El}{List\{Exp\}}}}}\terminal{;}}}}}
 \mequation{}{{\terminal{var}{\variable{X}{Id}}\terminal{;}}}{{\terminal{var}{{{\variable{X}{Id}}\terminal{=}{\constant{0}{Zero}}}}\terminal{;}}}
 \end{module}
\subsection{Basic Semantic Infrastructure}
 Before one starts adding semantic rules to a \K definition, one needs to
 define the basic semantic infrastructure consisting of definitions for {\em values},
 {\em computations} and the {\em configuration}.  The values are needed to know when to
 stop applying the heating rules corresponding to strictness or context declarations. As values
 carry semantic, language dependent meaning, they cannot be  automatically inferred, so one
 cannot avoid this step.  The computation structures, or simply computations, are needed to
 properly include the language syntax under the K sort, as the \K semantics operates only on
 terms of sort $K$; fortunately, this can be done mostly automatically, except for the special
 result computations.  Finally, the configuration serves as a backbone for the process of
 configuration abstraction which allows users to only mention the relevant cells in each
 semantic rule, the rest of the configuration context being inferred automatically. Although the
 configuration could potentially be automatically inferred from the rules, we believe that it is
 very useful for language designers/semanticists to actually think of and design their
 configuration explicitly, so the current implementation of \K requires one to define it.\\
 \begin{module}{\moduleName{SIMPLE-UNTYPED-SEMANTICS}}
 \including{\moduleName{K}\modulePlus{}\moduleName{SIMPLE-UNTYPED-DESUGARED-SYNTAX}}
 \sorts{\sort{List\{Val\}}\sort{Val}}
 \begin{latexComment}
  \subsubsection{Values}
 We here define the values of the language that the various fragments of
 programs evaluate to.  First, integers and Booleans are values.  As discussed,
 arrays evaluate to special array reference values holding (1) a location from where
 the array's elements are contiguously allocated in the store, and (2) the size
 of the array.  Functions evaluate to function values as $\lambda$-abstractions
 (we do not need to evaluate functions to closures because each function is executed
 in the fixed global environment and function definitions cannot be nested). 
 \end{latexComment}
 \syntax{\nonTerminal{\sort{Val}}}{\terminal{array(}{\nonTerminal{\sort{Nat}}}\terminal{,}{\nonTerminal{\sort{Nat}}}\terminal{)}}{}
 \syntaxCont{\nonTerminal{\sort{Val}}}{\crlbracket{\nonTerminal{\sort{Bool}}}}{}
 \syntaxCont{\nonTerminal{\sort{Val}}}{\crlbracket{\nonTerminal{\sort{Int}}}}{}
 \syntaxCont{\nonTerminal{\sort{Val}}}{\lambda{\nonTerminal{\sort{List\{Id\}}}}\,.\,{\nonTerminal{\sort{Stmt}}}}{}
 \syntax{\nonTerminal{\sort{Exp}}}{\crlbracket{\nonTerminal{\sort{Val}}}}{}
 \syntax{\nonTerminal{\sort{KResult}}}{\crlbracket{\nonTerminal{\sort{List\{Val\}}}}}{}
 \begin{latexComment}
  \subsection{Configuration}
 The \K configuration of SIMPLE consists of a top level cell, \textsf{T},
 holding a \textsf{threads} cell, a global environment map cell \textsf{genv}
 mapping the global variables and function names to their locations, a shared
 store map cell \textsf{store} mapping each location to some value, a set cell
 \textsf{busy} holding the locks which have been acquired but not yet released
 by threads, \textsf{input} and \textsf{output} list cells, and a
 \textsf{nextLoc} cell holding a natural number indicating the next available
 location.  For simplicity, the location counter in \textsf{nextLoc} models an actual physical location in the store (and assumes no garbage collection).  In other definitions (such as KERNELC) we show how one can model locations in the store to be symbolic and thus abstract away form the memory allocator library.   The \textsf{threads} cell contains
 one \textsf{thread} cell for each existing thread in the program.  Note that
 the thread cell has multiplicity ``*'', which means that at any given moment
 there could be zero, one or more \textsf{thread} cells.  Each \textsf{thread}
 cell contains a computation cell \textsf{k}, a \textsf{control} cell holding
 the various control structures needed to jump to certain points of interest
 in the program execution, a local environment map cell \textsf{env} mapping
 the thread local variables to locations in the store, and finally a
 \textsf{holds} map cell indicating what locks have been acquired by the thread
 and not released so far and how many times (SIMPLE's locks are re-entrant).
 The \textsf{control} cell currently contains only two subcells, a function
 stack \textsf{fstack} which is a list and an exception stack \textsf{xstack}
 which is also a list.  One can add more control structures in the
 \textsf{control} cell, such as a stack for break/continue of loops, etc., if
 the language is extended with more control-changing constructs.  Note that all
 cells except for \textsf{k} are also initialized, in that they contain a ground
 term of their corresponding sort.  The \textsf{k} cell needs not be initialized
 at this level, because it will be initialized with the program to evaluate later. 
 \end{latexComment}

\newpage

\kconfig[\hspace{-12em}]{\kallLarge{red}{T}{\kallLarge{orange}{threads}{\kallLarge{yellow}{thread *}{\kallLarge{green}{k}{\variable{K}{K}}\mathrel{}\kallLarge{violet}{env}{\dotCt{Map}}\mathrel{}\kallLarge{black}{holds}{\dotCt{Map}}\kBR\kallLarge{cyan}{control}{\kallLarge{blue}{fstack}{\dotCt{List}}\mathrel{}\kallLarge{purple}{xstack}{\dotCt{List}}}}}\mathrel{}\kBR \mathrel{}\kallLarge{pink}{genv}{\dotCt{Map}}\mathrel{}\kallLarge{white}{store}{\dotCt{Map}}\mathrel{}\kallLarge{cyan}{busy}{\dotCt{Set}}\kBR\mathrel{}\kallLarge{magenta}{in}{\dotCt{List}}\mathrel{}\kallLarge{brown}{out}{\dotCt{List}}\mathrel{}\kallLarge{gray}{nextLoc}{\constant{0}{Zero}}}}


 \begin{latexComment}
  \subsection{Variable Declaration}
 The SIMPLE syntax was desugared above so that each variable is declared alone and is also
 initialized.  The context declaration below says that the expression used for the initialization
 of the variable should be first evaluated (that expression can be any arithmetic expression,
 including array lookups, function calls, etc.).  The semantic rule below matches resulting
 variable declarations of the form ``$\texttt{var}\,X\,\texttt{=}\,V\texttt{;}$'' (with $V$ a
 value) on top of the \textsf{k} cell (indeed, note that the \textsf{k} cell is complete,
 or round, to the left, and is torn, or ruptured, to the right), allocates a fresh location
 $L$ in the store to hold the value $V$ (indeed, the unit ``$\kdot$'', or nothing, is matched
 anywhere in the map---note the tears at both sides---and replaced with the mapping
 $L\mapsto V$), and binds $X$ to $L$ in the local environment shadowing previous declarations
 of $X$, if any.  It is this possible shadowing of $X$ which disallows us to use a similar
 technique for updating the environment as for updating the store, as we know that $L$ is not
 already bound in the store when we add $L \mapsto V$.  We prefer the approach used for updating
 the store whenever possible, because it offers more true concurrency than the latter; indeed,
 according to the concurrent semantics of $K$, the store is not frozen while $L\mapsto V$ is
 added to it, while the environment is frozen during the update operation $\textit{Env}[L/X]$.
 The variable declaration command is also removed from the top of the computation cell
 and the fresh location counter is incremented.  All the above happen in one transactional step, with the rule
 below.  Note also how configuration abstraction allows us to only mention the needed cells;
 indeed, as the configuration above states, the \textsf{k} and \textsf{env} cells are actually
 located within a \textsf{thread} cell within the \textsf{threads} cell, but one needs not mention
 these: the configuration context of the rule is automatically transformed to match the declared
 configuration structure.
 \end{latexComment}
 \kcontext{}{\ensuremath{\terminal{var}{{{\variable{X}{Id}}\terminal{=}{\variable{\ensuremath{\square}}{List\{K\}}}}}\terminal{;}}}
 \krule{}{\ensuremath{{{{{{\kprefix{green}{k}{\reduce{{\terminal{var}{{{\variable{X}{Id}}\terminal{=}{\variable{V}{Val}}}}\terminal{;}}}{\dotCt{K}}}}\mathrel{\terminal{}}{\kall{violet}{env}{\reduce{\variable{Env}{Map}}{{{\variable{Env}{Map}}\mathrel{\terminal{[}}{\variable{L}{Nat}}\mathrel{\terminal{/}}{\variable{X}{Id}}\mathrel{\terminal{]}}}}}}}}\mathrel{\terminal{}}{\kmiddle{white}{store}{\reduce{\dotCt{Map}}{{{\variable{L}{Nat}}\mathrel{\terminal{\ensuremath{\mapsto}}}{\variable{V}{Val}}}}}}}}\mathrel{\terminal{}}{\kall{gray}{nextLoc}{\reduce{\variable{L}{Nat}}{{{\variable{L}{Nat}}\mathrel{\terminal{\ensuremath{{}+}\subscript{{\scriptstyle\it{}Nat}}}}{\constant{1}{Nat}}}}}}}}
 \begin{latexComment}
  \subsection{Array Declaration}
 The \K semantics of the uni-dimensional array declaration is somehow similar to the
 above declaration of ordinary variables.  $N+1$ locations are allocated in the store
 for an array of size $N$, the additional location (chosen to be the first one allocated)
 holding the array reference value.  The array reference value \texttt{array(L,N)} states
 that the array has size $N$ and its elements are located contiguously in the store starting
 with location $L$.  Recall that $L..L'$ is the list of locations between $L$ and $L'$
 and that $L..L'\mapsto V$ initializes each location in the list $L..L'$ to value $V$.  Note that, since the dimensions of array declarations can be arbitrary expressions, this virtually means that we can
 dynamically allocate memory in SIMPLE by means of array declarations. 
 \end{latexComment}
 \krule{}{\ensuremath{\kLarge{\kprefix{green}{k}{\reduce{{\terminal{var}{{{\variable{X}{Id}}\terminal{[}{\variable{N}{Nat}}\terminal{]}}}\terminal{;}}}{\dotCt{K}}}\mathrel{\terminal{}}\kall{violet}{env}{\reduce{\variable{Env}{Map}}{{{\variable{Env}{Map}}\mathrel{\terminal{[}}{\variable{L}{Nat}}\mathrel{\terminal{/}}{\variable{X}{Id}}\mathrel{\terminal{]}}}}}{\kall{gray}{nextLoc}{\reduce{\variable{L}{Nat}}{{{{{\variable{N}{Nat}}\mathrel{\terminal{\ensuremath{{}+}\subscript{{\scriptstyle\it{}Nat}}}}{\variable{L}{Nat}}}}\mathrel{\terminal{\ensuremath{{}+}\subscript{{\scriptstyle\it{}Nat}}}}{\constant{1}{Nat}}}}}}
 \mathrel{\terminal{}}
\kBR{\kmiddle{white}{store}{\reduce{\dotCt{Map}}{{{{{\variable{L}{Nat}}\mathrel{\terminal{\ensuremath{\mapsto}}}{{\terminal{array(}{{{\variable{L}{Nat}}\mathrel{\terminal{\ensuremath{{}+}\subscript{{\scriptstyle\it{}Nat}}}}{\constant{1}{Nat}}}}\terminal{,}{\variable{N}{Nat}}\terminal{)}}}}}\mathrel{\terminal{}}{{{{{{{\variable{L}{Nat}}\mathrel{\terminal{\ensuremath{{}+}\subscript{{\scriptstyle\it{}Nat}}}}{\constant{1}{Nat}}}}\terminal{..}{{{{{\variable{N}{Nat}}\mathrel{\terminal{\ensuremath{{}+}\subscript{{\scriptstyle\it{}Nat}}}}{\variable{L}{Nat}}}}\mathrel{\terminal{\ensuremath{{}+}\subscript{{\scriptstyle\it{}Nat}}}}{\constant{1}{Nat}}}}}}\mathrel{\terminal{\ensuremath{\mapsto}}}{\constant{0}{Zero}}}}}}}}}}}
 \begin{latexComment}
 SIMPLE allows multi-dimensional arrays.  For semantic simplicity, we desugar them all into
 uni-dimensional arrays by code transformation.  This way, we will only need to give semantics
 to uni-dimensional arrays.  First, the context rule below is used to request the evaluation of array dimensions: 
 \end{latexComment}
 \kcontext{}{\ensuremath{\terminal{var}{{{\variable{X}{Id}}\terminal{[}{{{{{\AnyVar{List\{K\}}}\terminal{,}{\variable{\ensuremath{\square}}{Exp}}}}\terminal{,}{\AnyVar{List\{K\}}}}}\terminal{]}}}\terminal{;}}}
 \begin{latexComment}
   Upon evaluating the array dimensions, the code generation rule below desugars multi-dimensional array declaration to uni-dimensional declarations. To this aim, we introduce two special unique variable
 identifiers, \texttt{\$1} and \texttt{\$2}.  The first, \texttt{\$1},
 is assigned the array reference value of the current array, so that we can redeclare
 the array inside the loop body with fewer dimensions.  The second variable,
 \texttt{\$2}, iterates through and initializes each element of the current dimension: 
 \end{latexComment}
 \syntax{\nonTerminal{\sort{Id}}}{\terminal{\$1}}{}
 \syntaxCont{\nonTerminal{\sort{Id}}}{\terminal{\$2}}{}
 \kequation{}{\ensuremath {\reduceTopS{\terminal{var}{{{\variable{X}{Id}}\terminal{[}{{{{\variable{\ensuremath{{N}_{1}}}{Nat}}\terminal{,}{\variable{\ensuremath{{N}_{2}}}{Nat}}}\terminal{,}{\variable{Vl}{List\{Val\}}}}}\terminal{]}}}\terminal{;}}{\begin{array}[t]{l}{\terminal{var}{{{\variable{X}{Id}}\terminal{[}{\variable{\ensuremath{{N}_{1}}}{Nat}}\terminal{]}}}\terminal{;}}
\kBR
 \mathrel{}\terminal{\{}{\begin{array}[t]{l}{{\terminal{var}{{{\constant{\ensuremath{\terminal{\$1}}}{Id}}\terminal{=}{\variable{X}{Id}}}}\terminal{;}}}\kBR \terminal{for}{\constant{\ensuremath{\terminal{\$2}}}{Id}}\terminal{=}{\constant{0}{Zero}}\terminal{to}{{{\variable{\ensuremath{{N}_{1}}}{Nat}}\terminal{-}{\constant{1}{Nat}}}}\terminal{do}\kBR\terminal{\{}{\begin{array}[t]{l} {{\terminal{var}{{{\variable{X}{Id}}\terminal{[}{{{\variable{\ensuremath{{N}_{2}}}{Nat}}\terminal{,}{\variable{Vl}{List\{Val\}}}}}\terminal{]}}}\terminal{;}}}\kBR{{{{{\constant{\ensuremath{\terminal{\$1}}}{Id}}\terminal{[}{\constant{\ensuremath{\terminal{\$2}}}{Id}}\terminal{]}}\terminal{=}{\variable{X}{Id}}}\terminal{;}}}\end{array}} \kBR \terminal{\}}\end{array}}\kBR\terminal{\}}\end{array}}}}
 \begin{latexComment}
  Ideally, one would like to perform syntactic desugarings like the one above before 
 the actual semantics.  Unfortunately, that was not possible in this case because the dimension expressions of the multi-dimensional array need to be evaluated first.
 Indeed, the desugaring rule above does not work if the dimensions of the declared
 array are arbitrary expressions, because they can have side effects
 (e.g., \texttt{a[++x,++x]}) and those side effects would be propagated each time the
 expression is evaluated in the desugaring code (note that both the loop condition and
 the nested multi-dimensional declaration would need to evaluate the expressions given as array dimensions). 
 \end{latexComment}
 \begin{latexComment}
  \subsection{Function declaration}
 Functions are evaluated to $\lambda$-abstractions and stored like any other values
 in the store.  A binding is added into the environment for the function name to the
 location holding its body.  Similarly to the C language, SIMPLE only allows function declarations at the top level
 of the program.  More precisely, the subsequent semantics of SIMPLE only works
 well when one respects this requirement.  Indeed, the simplistic context-free parser
 generated by the grammar above is more generous than we may want, in that it allows
 function declarations anywhere any declaration is allowed, including inside arbitrary
 blocks.  However, as the rule below shows, we are {\em not} storing the declaration
 environment with the $\lambda$-abstraction value as closures do.  Instead, as seen
 shortly, we switch to the global environment whenever functions are invoked, which
 is consistent with our requirement that functions should only be declared at the top.
 Thus, if one declares local functions, then one may see unexpected behaviors (e.g.,
 when one shadows a global variable before declaring a local function).  The type
 checker of SIMPLE, also defined in \K (see examples/simple/typed/static),
 discards programs which do not respect this requirement. 
 \end{latexComment}
 \krule{}{\ensuremath{{{{{{\kprefix{green}{k}{\reduce{{\terminal{function}{\variable{F}{Id}}\terminal{(}{\variable{Xl}{List\{Id\}}}\terminal{)}{\variable{S}{Stmt}}}}{\dotCt{K}}}}\mathrel{\terminal{}}{\kall{violet}{env}{\reduce{\variable{Env}{Map}}{{{\variable{Env}{Map}}\mathrel{\terminal{[}}{\variable{L}{Nat}}\mathrel{\terminal{/}}{\variable{F}{Id}}\mathrel{\terminal{]}}}}}}}}\mathrel{\terminal{}}{\kmiddle{white}{store}{\reduce{\dotCt{Map}}{{{\variable{L}{Nat}}\mathrel{\terminal{\ensuremath{\mapsto}}}{{\lambda{\variable{Xl}{List\{Id\}}}\,.\,{\variable{S}{Stmt}}}}}}}}}}\mathrel{\terminal{}}{\kall{gray}{nextLoc}{\reduce{\variable{L}{Nat}}{{{\variable{L}{Nat}}\mathrel{\terminal{\ensuremath{{}+}\subscript{{\scriptstyle\it{}Nat}}}}{\constant{1}{Nat}}}}}}}}
 \begin{latexComment}
  When we are done with the first pass (pre-processing), the computation cell
 \textsf{k} contains only the token \texttt{execute} (see the module
 SIMPLE-UNTYPED below, whose rule for initiating the execution of a program adds the token \texttt{execute}
 at the end of the program) and the cell \textsf{genv} is empty.  In this case, we
 have to call \texttt{main()} and to initialize the global environment by transferring the
 contents of the local environment into it.  We prefer to do it this way, as opposed to
 processing all the top level declarations directly within the global environment, because
 we want to avoid duplication of semantics: the syntax of the global declarations is
 identical to that of their corresponding local declarations, so the semantics of the latter
 suffices provided that we copy the local environment into the global one once we are done
 with the pre-processing.  We want this separate pre-processing step precisely because we
 want to create the global environment.  All (top-level) functions end up having their
 names bound in the global environment and, as seen below, they are executed in that same
 global environment; all these mean, in particular, that the functions ``see'' each other,
 allowing for mutual recursion, etc. 
 \end{latexComment}
 \syntax{\nonTerminal{\sort{K}}}{\terminal{execute}}{}
 \krule{}{\ensuremath{{{{\kall{green}{k}{\reduce{\constant{\ensuremath{\terminal{execute}}}{K}}{{{{{\constant{\ensuremath{\terminal{main}}}{Id}}\terminal{()}}}\terminal{;}}}}}\mathrel{\terminal{}}{\kall{violet}{env}{\variable{Env}{Map}}}}}\mathrel{\terminal{}}{\kall{pink}{genv}{\reduce{\dotCt{Map}}{\variable{Env}{Map}}}}}}
 \begin{latexComment}
  \section{Expressions}
 We next define the \K semantics of all the expression constructs, in the order in which
 their syntax was declared. 
 \end{latexComment}
 \begin{latexComment}
  \subsection{Variable lookup}
 When a variable $X$ is the first computational task (note the rupture of the \textsf{k} cell
 to the right), and $X$ is bound to some location $L$ in the environment (note the rupture of
 the \textsf{env} cell at both sides), and $L$ is mapped to some value $V$ in the store, then
 rewrite $X$ by $V$: 
 \end{latexComment}
 \krule{}{\ensuremath{{{{\kprefix{green}{k}{\reduce{\variable{X}{Id}}{\variable{V}{Val}}}}\mathrel{\terminal{}}{\kmiddle{violet}{env}{{{\variable{X}{Id}}\mathrel{\terminal{\ensuremath{\mapsto}}}{\variable{L}{Nat}}}}}}}\mathrel{\terminal{}}{\kmiddle{white}{store}{{{\variable{L}{Nat}}\mathrel{\terminal{\ensuremath{\mapsto}}}{\variable{V}{Val}}}}}}}
 \begin{latexComment}
  \subsection{Variable/Array increment}
 This is tricky, because we want to allow both {\tt ++x} and {\tt ++a[5]}.
 Therefore, we need to extract the l-value of the expression to increment.
 To do that, we state that the expression to increment should be wrapped
 by the auxiliary ``l-value'' operation and then evaluated.
 The semantics of the auxiliary l-value operation is defined below.
 For now, all we need to know is that it takes an expression and evaluates
 to a location value, also introduced below with the auxiliary operations.
 \end{latexComment}
 \kcontext{}{\ensuremath{\terminal{++}{\reduce{\variable{\ensuremath{\square}}{List\{K\}}}{{\terminal{l-value(}{\variable{\ensuremath{\square}}{List\{K\}}}\terminal{)}}}}}}
 \krule{}{\ensuremath{{\kprefix{green}{k}{\reduce{{\terminal{++}{{\terminal{loc(}{\variable{L}{Nat}}\terminal{)}}}}}{{{\variable{I}{Int}}\mathrel{\terminal{\ensuremath{{}+}\subscript{{\scriptstyle\it{}Int}}}}{\constant{1}{Nat}}}}}}\mathrel{\terminal{}}{\kmiddle{white}{store}{{{\variable{L}{Nat}}\mathrel{\terminal{\ensuremath{\mapsto}}}{\reduce{\variable{I}{Int}}{{{\variable{I}{Int}}\mathrel{\terminal{\ensuremath{{}+}\subscript{{\scriptstyle\it{}Int}}}}{\constant{1}{Nat}}}}}}}}}}
 \begin{latexComment}
  \subsection{Arithmetic operators}
 There is nothing special about the following rules.  They rewrite the language constructs to their
 library counterparts when their arguments become values of expected sorts: 
 \end{latexComment}
 \krule{}{\ensuremath \reduceTop{{{\variable{\ensuremath{{I}_{1}}}{Int}}\terminal{+}{\variable{\ensuremath{{I}_{2}}}{Int}}}}{{{\variable{\ensuremath{{I}_{1}}}{Int}}\mathrel{\terminal{\ensuremath{{}+}\subscript{{\scriptstyle\it{}Int}}}}{\variable{\ensuremath{{I}_{2}}}{Int}}}}}
 \krule{}{\ensuremath \reduceTop{{{\variable{\ensuremath{{I}_{1}}}{Int}}\terminal{-}{\variable{\ensuremath{{I}_{2}}}{Int}}}}{{{\variable{\ensuremath{{I}_{1}}}{Int}}\mathrel{\terminal{\ensuremath{{}-}\subscript{{\scriptstyle\it{}Int}}}}{\variable{\ensuremath{{I}_{2}}}{Int}}}}}
 \krule{}{\ensuremath \reduceTop{{{\variable{\ensuremath{{I}_{1}}}{Int}}\terminal{*}{\variable{\ensuremath{{I}_{2}}}{Int}}}}{{{\variable{\ensuremath{{I}_{1}}}{Int}}\mathrel{\terminal{*\subscript{{\scriptstyle\it{}Int}}}}{\variable{\ensuremath{{I}_{2}}}{Int}}}}}
 \kcrule{}{\ensuremath \reduceTop{{{\variable{\ensuremath{{I}_{1}}}{Int}}\terminal{/}{\variable{\ensuremath{{I}_{2}}}{Int}}}}{{{\variable{\ensuremath{{I}_{1}}}{Int}}\mathrel{\terminal{\ensuremath{{}\div}\subscript{{\scriptstyle\it{}Int}}}}{\variable{\ensuremath{{I}_{2}}}{Int}}}}}{\ensuremath{{\variable{\ensuremath{{I}_{2}}}{Int}}\mathrel{\terminal{$\neq$\subscript{{\scriptstyle\it{}Bool}}}}{\constant{0}{Zero}}}}
 \kcrule{}{\ensuremath \reduceTop{{{\variable{\ensuremath{{I}_{1}}}{Int}}\terminal{\%}{\variable{\ensuremath{{I}_{2}}}{Int}}}}{{{\variable{\ensuremath{{I}_{1}}}{Int}}\mathrel{\terminal{\%\subscript{{\scriptstyle\it{}Int}}}}{\variable{\ensuremath{{I}_{2}}}{Int}}}}}{\ensuremath{{\variable{\ensuremath{{I}_{2}}}{Int}}\mathrel{\terminal{$\neq$\subscript{{\scriptstyle\it{}Bool}}}}{\constant{0}{Zero}}}}
 \krule{}{\ensuremath \reduceTop{{\terminal{-}{\variable{I}{Int}}}}{{\mathrel{\terminal{\ensuremath{-{}}\subscript{{\scriptstyle\it{}Int}}}}{\variable{I}{Int}}}}}
 \krule{}{\ensuremath \reduceTop{{{\variable{\ensuremath{{I}_{1}}}{Int}}\terminal{<}{\variable{\ensuremath{{I}_{2}}}{Int}}}}{{{\variable{\ensuremath{{I}_{1}}}{Int}}\mathrel{\terminal{\ensuremath{<}\subscript{{\scriptstyle\it{}Int}}}}{\variable{\ensuremath{{I}_{2}}}{Int}}}}}
 \krule{}{\ensuremath \reduceTop{{{\variable{\ensuremath{{I}_{1}}}{Int}}\terminal{<=}{\variable{\ensuremath{{I}_{2}}}{Int}}}}{{{\variable{\ensuremath{{I}_{1}}}{Int}}\mathrel{\terminal{\ensuremath{\leq}\subscript{{\scriptstyle\it{}Int}}}}{\variable{\ensuremath{{I}_{2}}}{Int}}}}}
 \krule{}{\ensuremath \reduceTop{{{\variable{\ensuremath{{I}_{1}}}{Int}}\terminal{>}{\variable{\ensuremath{{I}_{2}}}{Int}}}}{{{\variable{\ensuremath{{I}_{1}}}{Int}}\mathrel{\terminal{\ensuremath{>}\subscript{{\scriptstyle\it{}Int}}}}{\variable{\ensuremath{{I}_{2}}}{Int}}}}}
 \krule{}{\ensuremath \reduceTop{{{\variable{\ensuremath{{I}_{1}}}{Int}}\terminal{>=}{\variable{\ensuremath{{I}_{2}}}{Int}}}}{{{\variable{\ensuremath{{I}_{1}}}{Int}}\mathrel{\terminal{\ensuremath{\geq}\subscript{{\scriptstyle\it{}Int}}}}{\variable{\ensuremath{{I}_{2}}}{Int}}}}}
 \krule{}{\ensuremath \reduceTop{{{\variable{\ensuremath{{V}_{1}}}{Val}}\terminal{==}{\variable{\ensuremath{{V}_{2}}}{Val}}}}{{{\variable{\ensuremath{{V}_{1}}}{Val}}\mathrel{\terminal{$=$\subscript{{\scriptstyle\it{}Bool}}}}{\variable{\ensuremath{{V}_{2}}}{Val}}}}}
 \krule{}{\ensuremath \reduceTop{{{\variable{\ensuremath{{V}_{1}}}{Val}}\terminal{!=}{\variable{\ensuremath{{V}_{2}}}{Val}}}}{{{\variable{\ensuremath{{V}_{1}}}{Val}}\mathrel{\terminal{$\neq$\subscript{{\scriptstyle\it{}Bool}}}}{\variable{\ensuremath{{V}_{2}}}{Val}}}}}
 \krule{}{\ensuremath \reduceTop{{{\variable{\ensuremath{{T}_{1}}}{Bool}}\terminal{and}{\variable{\ensuremath{{T}_{2}}}{Bool}}}}{{{\variable{\ensuremath{{T}_{1}}}{Bool}}\mathrel{\terminal{$\wedge$\subscript{{\scriptstyle\it{}Bool}}}}{\variable{\ensuremath{{T}_{2}}}{Bool}}}}}
 \krule{}{\ensuremath \reduceTop{{{\variable{\ensuremath{{T}_{1}}}{Bool}}\terminal{or}{\variable{\ensuremath{{T}_{2}}}{Bool}}}}{{{\variable{\ensuremath{{T}_{1}}}{Bool}}\mathrel{\terminal{$\vee$\subscript{{\scriptstyle\it{}Bool}}}}{\variable{\ensuremath{{T}_{2}}}{Bool}}}}}
 \krule{}{\ensuremath \reduceTop{{\terminal{not}{\variable{T}{Bool}}}}{{\mathrel{\terminal{$\neg$\subscript{{\scriptstyle\it{}Bool}}}}{\variable{T}{Bool}}}}}
 \begin{latexComment}
  \subsection{Array lookup}
 Untyped SIMPLE does not check array bounds (the dynamically typed version of it, in
 examples/simple/typed/dynamic, does check for array out of bounds).  The first rule below
 desugars multi-dimensional array access to uni-dimensional array access; recall that the
 array access operation was declared strict, so all sub-expressions involved are already
 values at this stage.  The second rule rewrites the array access to a lookup operation
 at a precise location; we prefer to do it this way to avoid locking the store.
 Recall that ``---'' is an anonymous variable in \K matching any subterm (like in Prolog);
 informally, ``there is something there but we don't care what''.
 The semantics of the \texttt{lookup} operation is straightforward. 
 \end{latexComment}
 \kequation{}{\ensuremath \reduceTopS{{{\variable{V}{Val}}\terminal{[}{{{{{\variable{\ensuremath{{N}_{1}}}{Nat}}\terminal{,}{\variable{\ensuremath{{N}_{2}}}{Nat}}}}\terminal{,}{\variable{Vl}{List\{Val\}}}}}\terminal{]}}}{{{{{\variable{V}{Val}}\terminal{[}{\variable{\ensuremath{{N}_{1}}}{Nat}}\terminal{]}}}\terminal{[}{{{\variable{\ensuremath{{N}_{2}}}{Nat}}\terminal{,}{\variable{Vl}{List\{Val\}}}}}\terminal{]}}}}
 \syntax{\nonTerminal{\sort{K}}}{\terminal{lookup(}{\nonTerminal{\sort{Nat}}}\terminal{)}}{}
 \kequation{}{\ensuremath \reduceTopS{{{{\terminal{array(}{\variable{L}{Nat}}\terminal{,}{\AnyVar{List\{K\}}}\terminal{)}}}\terminal{[}{\variable{N}{Nat}}\terminal{]}}}{{\terminal{lookup(}{{{\variable{N}{Nat}}\mathrel{\terminal{\ensuremath{{}+}\subscript{{\scriptstyle\it{}Int}}}}{\variable{L}{Nat}}}}\terminal{)}}}}
 \krule{}{\ensuremath{{\kprefix{green}{k}{\reduce{{\terminal{lookup(}{\variable{L}{Nat}}\terminal{)}}}{\variable{V}{Val}}}}\mathrel{\terminal{}}{\kmiddle{white}{store}{{{\variable{L}{Nat}}\mathrel{\terminal{\ensuremath{\mapsto}}}{\variable{V}{Val}}}}}}}
 \begin{latexComment}
  \subsection{Size of an array}
 The size of the array is stored in the array reference value, and the \texttt{sizeOf} construct
 was declared strict, so: 
 \end{latexComment}
 \krule{}{\ensuremath \reduceTop{{\terminal{sizeOf(}{{\terminal{array(}{\AnyVar{List\{K\}}}\terminal{,}{\variable{N}{Nat}}\terminal{)}}}\terminal{)}}}{\variable{N}{Nat}}}
 \begin{latexComment}
  \subsection{Function call}
 Function application was strict in both its arguments, so we can assume that both
 the function and its arguments are evaluated to values (the former expected to be a
 $\lambda$-abstraction).  The first rule below matches a well-formed function application
 on top of the computation and performs the following steps atomically: it switches to the
 function body followed by ``\texttt{return 0;}'' (here 0 is a default return value for
 the case in which the function does not use an explicit return statement); it pushes the
 remaining computation, the current environment, and the current control data onto the
 function stack (the remaining computation can thus also be discarded from the computation
 cell, because an unavoidable subsequent \texttt{return} statement---see above---will always
 recover it from the stack); it switches the current environment (which is being pushed on
 the function stack) to the global environment, which is where the free variables in the
 function body should be looked up; it binds the formal parameters to fresh locations in
 the new environment, and stores the actual arguments to those locations in the store.
 The second rule pops the computation, the environment and the control data from the
 function stack when a \texttt{return} statement is encountered as the next computational
 task, passing the returned value to the popped computation (the popped computation was
 the context in which the returning function was called). 
 \end{latexComment}
 \syntax{\nonTerminal{\sort{ListItem}}}{\terminal{(}{\nonTerminal{\sort{Map}}}\terminal{,}{\nonTerminal{\sort{K}}}\terminal{,}{\nonTerminal{\sort{Bag}}}\terminal{)}}{}
 \krule{}{\ensuremath{\kLarge{{{{\kall{green}{k}{\reduce{{{{{{\lambda{\variable{Xl}{List\{Id\}}}\,.\,{\variable{S}{Stmt}}}}\terminal{(}{\variable{Vl}{List\{Val\}}}\terminal{)}}}\mathrel{\terminal{\ensuremath{\kra}}}{\variable{K}{K}}}}{{{\variable{S}{Stmt}}\mathrel{\terminal{\ensuremath{\kra}}}{{\terminal{return}{\constant{0}{Zero}}\terminal{;}}}}}}}\mathrel{\terminal{}}{\kall{cyan}{control}{{{\kprefix{blue}{fstack}{\reduce{\dotCt{List}}{{\terminal{(}{\variable{Env}{Map}}\terminal{,}{\variable{K}{K}}\terminal{,}{\variable{C}{Bag}}\terminal{)}}}}}\mathrel{\terminal{}}{\variable{C}{Bag}}}}}}}\mathrel{\terminal{}} \kBR{\kall{violet}{env}{\reduce{\variable{Env}{Map}}{{{\variable{GEnv}{Map}}\mathrel{\terminal{[}}{{{\variable{N}{Nat}}\terminal{..}{{{\variable{N}{Nat}}\mathrel{\terminal{\ensuremath{{}+}\subscript{{\scriptstyle\it{}Nat}}}}{{\mid\!\!{\variable{Xl}{List\{Id\}}}\!\mid}}}}}}\mathrel{\terminal{/}}{{{\variable{Xl}{List\{Id\}}}}}\mathrel{\terminal{]}}}}}}\mathrel{\terminal{}}{\kall{pink}{genv}{\variable{GEnv}{Map}}}\mathrel{\terminal{}}\kBR {\kmiddle{white}{store}{\reduce{\dotCt{Map}}{{{{{\variable{N}{Nat}}\terminal{..}{{{\variable{N}{Nat}}\mathrel{\terminal{\ensuremath{{}+}\subscript{{\scriptstyle\it{}Nat}}}}{{\mid\!\!{\variable{Xl}{List\{Id\}}}\!\mid}}}}}}\mathrel{\terminal{\ensuremath{\mapsto}}}{{{\variable{Vl}{List\{Val\}}}}}}}}}\mathrel{\terminal{}}{\kall{gray}{nextLoc}{\reduce{\variable{N}{Nat}}{{{\variable{N}{Nat}}\mathrel{\terminal{\ensuremath{{}+}\subscript{{\scriptstyle\it{}Nat}}}}{{\mid\!\!{\variable{Xl}{List\{Id\}}}\!\mid}}}}}}}}}
 \krule{}{\ensuremath{{{{\kall{green}{k}{\reduce{{{{\terminal{return}{\variable{V}{Val}}\terminal{;}}}\mathrel{\terminal{\ensuremath{\kra}}}{\AnyVar{List\{K\}}}}}{{{\variable{V}{Val}}\mathrel{\terminal{\ensuremath{\kra}}}{\variable{K}{K}}}}}}\mathrel{\terminal{}}{\kall{cyan}{control}{{{\kprefix{blue}{fstack}{\reduce{{\terminal{(}{\variable{Env}{Map}}\terminal{,}{\variable{K}{K}}\terminal{,}{\variable{C}{Bag}}\terminal{)}}}{\dotCt{List}}}}\mathrel{\terminal{}}{\reduce{\AnyVar{Bag}}{\variable{C}{Bag}}}}}}}}\mathrel{\terminal{}}{\kall{violet}{env}{\reduce{\AnyVar{Map}}{\variable{Env}{Map}}}}}}
 \begin{latexComment}
  \subsection{Read}
 The \texttt{read()} expression construct simply evaluates to the next input value, at the
 same time discarding the input value from the \textsf{in} cell.  In an implementation of the
 SIMPLE language, one would likely want to make the input buffer interactive, prompting the
 user to provide a new value whenever needed.  In a semantics, however, it is acceptable to
 assume that all the input values are given before the program is executed; thus, the
 rewrite process gets stuck if the next computation item is a \texttt{read()} expression
 construct and no input item is available. 
 \end{latexComment}
 \krule{}{\ensuremath{{\kprefix{green}{k}{\reduce{\constant{\ensuremath{\terminal{read()}}}{Exp}}{\variable{I}{Int}}}}\mathrel{\terminal{}}{\kprefix{magenta}{in}{\reduce{{{\variable{I}{Int}}}}{\dotCt{List}}}}}}
 \begin{latexComment}
  \subsection{Assignment}
 In SIMPLE, like in C, assignments are expression constructs and not statement constructs.
 To make it a statement all one needs to do is to follow it by a semi-colon ``\texttt{;}''
 (see the semantics for expression statements below).
 Like for the increment, we want to allow assignments not only to variables but also to array
 elements, e.g., \texttt{e1[e2] = e3} where \texttt{e1} evaluates to an array reference,
 \texttt{e2} to a natural number, and \texttt{e3} to any value.  Thus, we first compute the
 l-value of the left-hand-side expression that appears in an assignment.  Like for the
 increment, all we need to know is that \texttt{l-value(...)} eventually evaluates to a
 location value \texttt{loc(...)}. 
 \end{latexComment}
 \kcontext{}{\ensuremath{{\reduce{\variable{\ensuremath{\square}}{List\{K\}}}{{\terminal{l-value(}{\variable{\ensuremath{\square}}{List\{K\}}}\terminal{)}}}}\terminal{=}{\AnyVar{List\{K\}}}}}
 \krule{}{\ensuremath{{\kprefix{green}{k}{\reduce{{{{\terminal{loc(}{\variable{L}{Nat}}\terminal{)}}}\terminal{=}{\variable{V}{Val}}}}{\variable{V}{Val}}}}\mathrel{\terminal{}}{\kmiddle{white}{store}{{{\variable{L}{Nat}}\mathrel{\terminal{\ensuremath{\mapsto}}}{\reduce{\AnyVar{List\{K\}}}{\variable{V}{Val}}}}}}}}
 \begin{latexComment}
  \section{Statements}
 We next define the \K semantics of statements, also in the order their syntax was given.
 \end{latexComment}
 \begin{latexComment}
  \subsection{Blocks}
 Empty blocks are simply discarded, as shown in the first rule below.
 For non-empty blocks, we schedule the enclosed statement but we have to
 make sure the environment is recovered after the enclosed statement executes.
 Recall that we allow local variable declarations, whose scope is the block enclosing them.
 That is the reason for which we have to recover the environment after the block.
 This allows us to have a very simple semantics for variable declarations, as we did above.
 One can make the two rules below computational if one wants them to count as
 computational steps. 
 \end{latexComment}
 \kequation{}{\ensuremath \reduceTopS{\constant{\ensuremath{\terminal{\{\}}}}{Stmt}}{\dotCt{K}}}
 \kequation{}{\ensuremath{{\kprefix{green}{k}{\reduceS{{\terminal{\{}{\variable{Ss}{Stmts}}\terminal{\}}}}{{{\variable{Ss}{Stmts}}\mathrel{\terminal{\ensuremath{\kra}}}{{\terminal{env(}{\variable{Env}{Map}}\terminal{)}}}}}}}\mathrel{\terminal{}}{\kall{violet}{env}{\variable{Env}{Map}}}}}
 \begin{latexComment}
  The definition of environment recovery is straightforward: 
 \end{latexComment}
 \syntax{\nonTerminal{\sort{K}}}{\terminal{env(}{\nonTerminal{\sort{Map}}}\terminal{)}}{}
 \kequation{}{\ensuremath{{\kprefix{green}{k}{\reduceS{{\terminal{env(}{\variable{Env}{Map}}\terminal{)}}}{\dotCt{K}}}}\mathrel{\terminal{}}{\kall{violet}{env}{\reduceS{\AnyVar{Map}}{\variable{Env}{Map}}}}}}
 \begin{latexComment}
 There are two common alternatives to the above semantics of blocks.  One is to keep track of
 the variables which are declared in the block and only recover those at the end of the block.
 This way one does more work for variable declarations but conceptually less work for environment
 recovery; we say ``conceptually'' because it is not clear that it is indeed the case that one does
 less work when AC matching is involved.  The other alternative is to work with a stack of
 environments instead of a flat environment, and push the current environment when entering a block
 and pop it when exiting it.  This way, one does more work when accessing variables (since one has
 to search the variable in the environment stack in a top-down manner), but on the other hand uses
 smaller environments and the definition gets closer to an implementation.  Based on experience with
 dozens of language semantics and other \K definitions, we have found that our approach above is the
 best trade-off between elegance and efficiency (especially since rewrite engines have built-in techniques to lazily copy terms, by need, thus not creating unnecessary copies) , so it is the one that we follow in general.  
 \end{latexComment}
 \begin{latexComment}
  \subsection{Sequential composition}
 Sequential composition is desugared into \K's builtin sequentialization operation (recall that, like in C,
 the semi-colon ``\texttt{;}'' is not a statement separator in SIMPLE---it is either a statement
 terminator or a construct for a statement from an expression).
 The rule below is computational, so it does count as a computational step.
 One can make it structural if one does not want it to count as a step.
 Note that \K allows to define the semantics of SIMPLE in such a way that statements eventually
 dissolve from the top of the computation when they are completed; this is in sharp contrast to
 (artificially) ``evaluating'' them to a special \texttt{skip} statement value and then getting
 rid of that special value, as it is the case in other semantic approaches (where everything
 must evaluate to something).  This means that once $S_1$ completes in the rule below, $S_2$
 becomes automatically the next computation item without any additional (explicit or implicit)
 rules. 
 \end{latexComment}
 \krule{}{\ensuremath \reduceTop{{{\variable{\ensuremath{{S}_{1}}}{Stmt}}\mathrel{}{\variable{\ensuremath{{S}_{2}}}{Stmt}}}}{{{\variable{\ensuremath{{S}_{1}}}{Stmt}}\mathrel{\terminal{\ensuremath{\kra}}}{\variable{\ensuremath{{S}_{2}}}{Stmt}}}}}
 \begin{latexComment}
  \subsection{Expression statements}
 Expression statements are only used for their side effects, so their result value
 is simply discarded.  Common examples of expression statements are ones of the form
 ``\texttt{++x;}'', ``\texttt{x=e;}'', ``\texttt{e1[e2]=e3;}'', etc. 
 \end{latexComment}
 \krule{}{\ensuremath \reduceTop{{{\variable{V}{Val}}\terminal{;}}}{\dotCt{K}}}
 \begin{latexComment}
  \subsection{Conditional}
 Since the conditional was declared with the \texttt{strict(1)} attribute, we can assume
 that its first argument will eventually be evaluated.  The rules below cover the only
 two possibilities in which the conditional is allowed to proceed (otherwise the rewriting process
 gets stuck). 
 \end{latexComment}
 \krule{}{\ensuremath \reduceTop{{\terminal{if}{\constant{true}{Bool}}\terminal{then}{\variable{S}{Stmt}}\terminal{else}{\AnyVar{List\{K\}}}}}{\variable{S}{Stmt}}}
 \krule{}{\ensuremath \reduceTop{{\terminal{if}{\constant{false}{Bool}}\terminal{then}{\AnyVar{List\{K\}}}\terminal{else}{\variable{S}{Stmt}}}}{\variable{S}{Stmt}}}
 \begin{latexComment}
  \subsection{While loop}
 The simplest way to give the semantics of the while loop is by unrolling.
 Note, however, that its unrolling is only allowed when the while loop reaches the top of the
 computation (to avoid non-termination of unrolling).  We prefer the rule below to be structural,
 because we don't want the unrolling of the while loop to count as a computational step; this is
 unavoidable in conventional semantics, but it is possible in \K thanks to its distinction between
 structural and computational rules.  The simple while loop semantics below works because our
 while loops in SIMPLE are indeed very basic.  If we allowed break/continue of loops then we
 would need a completely different semantics, which would also involve the \textsf{control} cell. 
 \end{latexComment}
 \kequation{}{\ensuremath \kprefix{green}{k}{\reduceS{{\terminal{while}{\variable{B}{Exp}}\terminal{do}{\variable{S}{Stmt}}}}{{\terminal{if}{\variable{B}{Exp}}\terminal{then}{{\terminal{\{}{{{\variable{S}{Stmt}}\mathrel{}{{\terminal{while}{\variable{B}{Exp}}\terminal{do}{\variable{S}{Stmt}}}}}}\terminal{\}}}}\terminal{else}{\constant{\ensuremath{\terminal{\{\}}}}{Stmt}}}}}}
 \begin{latexComment}
  \subsection{Write}
 The write statement appends its evaluated argument (recall that \texttt{write} was declared strict)
 to the output list.  Like in the case of the \texttt{read()} construct, implementations of SIMPLE
 may choose to display the output incrementally, as it is being generated; in semantics, we do not
 need to worry about that and simply collect all the output in the \textsf{out} cell. 
 \end{latexComment}
 \krule{}{\ensuremath{{\kprefix{green}{k}{\reduce{{\terminal{write(}{\variable{I}{Int}}\terminal{);}}}{\dotCt{K}}}}\mathrel{\terminal{}}{\ksuffix{brown}{out}{\reduce{\dotCt{List}}{{{\variable{I}{Int}}}}}}}}
 \begin{latexComment}
  \subsection{Exceptions}
 SIMPLE allows parametric exceptions, in that one can throw and catch a particular value.
 The statement ``\texttt{try $S_1$ catch($X$) $S_2$}'' proceeds with the evaluation of 
 $S_1$.  If $S_1$ evaluates normally, i.e., without any exception thrown, then $S_2$ is
 discarded and the execution continues normally.  If $S_1$ throws an exception with a
 statement of the form ``\texttt{throw $E$}'', then $E$ is first evaluated to some value $V$
 (\texttt{throw} was declared to be strict), then $V$ is bound to $X$, then $S_2$ is evaluated
 in the new environment while the reminder of $S_1$ is discarded, then the environment is recovered
 and the execution continues normally with the statement following the
 ``\texttt{try $S_1$ catch($X$) $S_2$}'' statement.  Exceptions can be nested and
 the statements in the ``\texttt{catch}'' part ($S_2$ in our case) can throw exceptions to the
 upper level.  One should be careful with how one handles the control data structures here, so that
 the abrupt changes of control due to exception throwing and to function returns interact correctly
 with each other.  For example, we want to allow function calls inside the statement
 $S_1$ in a ``\texttt{try $S_1$ catch($X$) $S_2$}'' block which can throw an exception that is not
 caught by the function but instead is propagated to the ``\texttt{try $S_1$ catch($X$) $S_2$}'' block
 that called the function.  Therefore, we have to make sure that the function stack as well as other
 potential control structures are also properly modified when the exception is thrown to
 correctly recover the execution context.  This can be easily achieved by pushing/popping the
 entire current control context onto the exception stack.  The three rules below modularly do
 precisely all the above. 
 \end{latexComment}
 \syntax{\nonTerminal{\sort{ListItem}}}{\terminal{(}{\nonTerminal{\sort{Id}}}\terminal{,}{\nonTerminal{\sort{Stmt}}}\terminal{,}{\nonTerminal{\sort{K}}}\terminal{,}{\nonTerminal{\sort{Map}}}\terminal{,}{\nonTerminal{\sort{Bag}}}\terminal{)}}{}
 \syntax{\nonTerminal{\sort{K}}}{\terminal{popx}}{}

\krule{}{\ensuremath{\kLarge{{{\kall{green}{k}{{{\reduce{{\terminal{try}{\variable{\ensuremath{{S}_{1}}}{Stmt}}\terminal{catch(}{\variable{X}{Id}}\terminal{)}{\variable{\ensuremath{{S}_{2}}}{Stmt}}}}{{{\variable{\ensuremath{{S}_{1}}}{Stmt}}\mathrel{\terminal{\ensuremath{\kra}}}{\constant{\ensuremath{\terminal{popx}}}{K}}}}}\mathrel{\terminal{\ensuremath{\kra}}}{\variable{K}{K}}}}}\mathrel{\terminal{}}{\kall{violet}{env}{\variable{Env}{Map}}}} \kBR \mathrel{\terminal{}}{\kall{cyan}{control}{{{\kprefix{purple}{xstack}{\reduce{\dotCt{List}}{{\terminal{(}{\variable{X}{Id}}\terminal{,}{\variable{\ensuremath{{S}_{2}}}{Stmt}}\terminal{,}{\variable{K}{K}}\terminal{,}{\variable{Env}{Map}}\terminal{,}{\variable{C}{Bag}}\terminal{)}}}}}\mathrel{\terminal{}}{\variable{C}{Bag}}}}}}}}
 \krule{}{\ensuremath{{\kprefix{green}{k}{\reduce{\constant{\ensuremath{\terminal{popx}}}{K}}{\dotCt{K}}}}\mathrel{\terminal{}}{\kprefix{purple}{xstack}{\reduce{\AnyVar{ListItem}}{\dotCt{List}}}}}}
 \krule{}{\ensuremath{\kLarge{{{\kall{green}{k}{\reduce{{{{\terminal{throw}{\variable{V}{Val}}\terminal{;}}}\mathrel{\terminal{\ensuremath{\kra}}}{\AnyVar{List\{K\}}}}}{{{{\terminal{\{}{{{{\terminal{var}{{{\variable{X}{Id}}\terminal{=}{\variable{V}{Val}}}}\terminal{;}}}\mathrel{}{\variable{\ensuremath{{S}_{2}}}{Stmt}}}}\terminal{\}}}}\mathrel{\terminal{\ensuremath{\kra}}}{\variable{K}{K}}}}}}\mathrel{\terminal{}}  {\kall{violet}{env}{\reduce{\AnyVar{Map}}{\variable{Env}{Map}}}}} \kBR \mathrel{\terminal{}}
 {\kall{cyan}{control}{{{\kprefix{purple}{xstack}{\reduce{{\terminal{(}{\variable{X}{Id}}\terminal{,}{\variable{\ensuremath{{S}_{2}}}{Stmt}}\terminal{,}{\variable{K}{K}}\terminal{,}{\variable{Env}{Map}}\terminal{,}{\variable{C}{Bag}}\terminal{)}}}{\dotCt{List}}}}\mathrel{\terminal{}}{\reduce{\AnyVar{Bag}}{\variable{C}{Bag}}}}}}}}}

\begin{latexComment}
  The catch statement $S_2$ needs to be executed in the original environment, but where the thrown value $V$ was bound to the catch variable $X$.  We here chose to rely on two previously defined constructs when giving semantics to the catch part of the statement: (1) the variable declaration with initialization, for binding $X$ for $V$; and (2) the block construct for preventing $X$ from shadowing variables in the original environment upon the completion of $S_2$. 
 Note, however, that the semantics of {\tt throw} can also be given directly, in one computational step, especially in languages without variable initializers and blocks.
 \end{latexComment}
 \begin{latexComment}
  \subsection{Threads}
 SIMPLE's threads can be created and terminated dynamically, and can synchronize by
 acquiring and releasing re-entrant locks and by rendezvous.  We discuss the 7 rules
 giving the semantics of these operations below. 
 \end{latexComment}
 \begin{latexComment}
  \subsubsection{Thread creation}
 Threads can be created by any other threads using the ``\texttt{spawn $S$}'' statement.
 The spawn statement is consumed in the creating thread and, at the same time,  a new thread
 cell  is added to the to the configuration initialized with the $S$ statement and sharing the same environment with the spawning thread.  Note that the newly created \textsf{thread}
 cell is torn.  That means that the remaining cells are added and initialized automatically as
 described in the definition of SIMPLE's configuration.  This is part of \K's
 configuration abstraction/concretization mechanism. 
 \end{latexComment}
 \krule{}{\ensuremath{{\kmiddle{yellow}{thread}{{{\kprefix{green}{k}{\reduce{{\terminal{spawn}{\variable{S}{Stmt}}}}{\dotCt{K}}}}\mathrel{\terminal{}}{\kall{violet}{env}{\variable{Env}{Map}}}}}}\mathrel{\terminal{}}{\reduce{\dotCt{Bag}}{\kmiddle{yellow}{thread}{{{\kall{green}{k}{\variable{S}{Stmt}}}\mathrel{\terminal{}}{\kall{violet}{env}{\variable{Env}{Map}}}}}}}}}
 \begin{latexComment}
  \subsubsection{Thread termination}
 Dually to the above, when a thread terminates its assigned computation (the contents of its
 \textsf{k} cell) is empty, so the thread can be dissolved.  However, since no discipline is imposed on how
 locks are acquired and released, it can be the case that a terminating thread still holds
 locks.  Those locks must be released, so other threads attempting to acquire them do not deadlock.
 We achieve that by removing all the locks held by the terminating thread in its \textsf{holds}
 cell from the set of busy locks in the \textsf{busy} cell (\texttt{keys($H$)} returns the domain
 of the map $H$ as a set, that is, only the locks themselves ignoring their multiplicity).
 As seen below, a lock is added to the \textsf{busy} cell as soon as it is acquired
 for the first time by a thread. 
 \end{latexComment}
 \krule{}{\ensuremath{{\reduce{\kmiddle{yellow}{thread}{{{\kall{green}{k}{\dotCt{K}}}\mathrel{\terminal{}}{\kall{black}{holds}{\variable{H}{Map}}}}}}{\dotCt{Bag}}}\mathrel{\terminal{}}{\kall{cyan}{busy}{\reduce{\variable{Busy}{Set}}{{{\variable{Busy}{Set}}\mathrel{\terminal{-\subscript{{\scriptstyle\it{}Set}}}}{{\mathrel{\terminal{keys}}{\variable{H}{Map}}}}}}}}}}
 \begin{latexComment}
  \subsubsection{Acquire lock}
 There are two cases to distinguish when a thread attempts to acquire a lock (in SIMPLE any value
 can be used as a lock):
 (1) The thread does not currently have the lock, in which case it has to
 take it provided that the lock is not already taken by another thread (see
 the side condition of the first rule).
 (2) The thread already has the lock, in which case it just increments its counter
 for the lock (the locks are re-entrant).
 These two cases are captured by the two rules below: 
 \end{latexComment}
 \kcrule{}{\ensuremath{{{{\kprefix{green}{k}{\reduce{{\terminal{acquire}{\variable{V}{Val}}\terminal{;}}}{\dotCt{K}}}}\mathrel{\terminal{}}{\kmiddle{black}{holds}{\reduce{\dotCt{Map}}{{{\variable{V}{Val}}\mathrel{\terminal{\ensuremath{\mapsto}}}{\constant{0}{Zero}}}}}}}}\mathrel{\terminal{}}{\kall{cyan}{busy}{{{\variable{Busy}{Set}}\mathrel{\terminal{}}{\reduce{\dotCt{Set}}{{{\variable{V}{Val}}}}}}}}}}{\ensuremath{\mathrel{\terminal{$\neg$\subscript{{\scriptstyle\it{}Bool}}}}{{{\variable{V}{Val}}\mathrel{\terminal{in}}{\variable{Busy}{Set}}}}}}
 \krule{}{\ensuremath{{\kprefix{green}{k}{\reduce{{\terminal{acquire}{\variable{V}{Val}}\terminal{;}}}{\dotCt{K}}}}\mathrel{\terminal{}}{\kmiddle{black}{holds}{{{\variable{V}{Val}}\mathrel{\terminal{\ensuremath{\mapsto}}}{\reduce{\variable{N}{Nat}}{{{\variable{N}{Nat}}\mathrel{\terminal{\ensuremath{{}+}\subscript{{\scriptstyle\it{}Nat}}}}{\constant{1}{Nat}}}}}}}}}}
 \begin{latexComment}
  \subsubsection{Release lock}
 Similarly, there are two corresponding cases to distinguish when a thread releases a lock:
 (1) The thread holds the lock more than once, in which case all it needs to do is to decrement
 the lock counter.
 (2) The thread holds the lock only once, in which case it needs to remove it from its
 \textsf{holds} cell and also from the the shared \textsf{busy} cell, so other threads can
 acquire it if they need to. 
 \end{latexComment}
 \kcrule{}{\ensuremath{{\kprefix{green}{k}{\reduce{{\terminal{release}{\variable{V}{Val}}\terminal{;}}}{\dotCt{K}}}}\mathrel{\terminal{}}{\kmiddle{black}{holds}{{{\variable{V}{Val}}\mathrel{\terminal{\ensuremath{\mapsto}}}{\reduce{\variable{N}{Nat}}{{{\variable{N}{Nat}}\mathrel{\terminal{\ensuremath{{}-}\subscript{{\scriptstyle\it{}Int}}}}{\constant{1}{Nat}}}}}}}}}}{\ensuremath{{\variable{N}{Nat}}\mathrel{\terminal{\ensuremath{{}>}\subscript{{\scriptstyle\it{}Nat}}}}{\constant{0}{Zero}}}}
 \krule{}{\ensuremath{{{{\kprefix{green}{k}{\reduce{{\terminal{release}{\variable{V}{Val}}\terminal{;}}}{\dotCt{K}}}}\mathrel{\terminal{}}{\kmiddle{black}{holds}{\reduce{{{\variable{V}{Val}}\mathrel{\terminal{\ensuremath{\mapsto}}}{\constant{0}{Zero}}}}{\dotCt{Map}}}}}}\mathrel{\terminal{}}{\kmiddle{cyan}{busy}{\reduce{{{\variable{V}{Val}}}}{\dotCt{Set}}}}}}
 \begin{latexComment}
  \subsubsection{Rendezvous synchronization}
 In addition to synchronization through acquire and release of locks, SIMPLE also provides
 a construct for rendezvous synchronization.  A thread whose next statement to execute is
 \texttt{rendezvous($V$)} gets stuck until another thread reaches an identical statement;
 when that happens, the two threads drop their rendezvous statements and continue their
 executions.  If three threads happen to have an identical rendezvous statement as
 their next statement, then precisely two of them will synchronize and the other will
 remain blocked until another thread reaches a similar rendezvous statement.  The rule
 below is as simple as it can get.  Note, however, that, again, it is \K's mechanism for
 configuration abstraction that makes it work as desired: since the only cell which can
 multiply containing a \textsf{k} cell inside is the \textsf{thread} cell, the only way
 to concretize the rule below to the actual configuration of SIMPLE is to include each
 \textsf{k} cell in a \textsf{thread} cell. 
 \end{latexComment}
 \krule{}{\ensuremath{{\kprefix{green}{k}{\reduce{{\terminal{rendezvous}{\variable{V}{Val}}\terminal{;}}}{\dotCt{K}}}}\mathrel{\terminal{}}{\kprefix{green}{k}{\reduce{{\terminal{rendezvous}{\variable{V}{Val}}\terminal{;}}}{\dotCt{K}}}}}}
 \begin{latexComment}
\subsection{l-value and loc}
 For convenience in giving the semantics of constructs like the increment and the assignment, that
 we want to operate the same way on variables and on array elements, we used an auxiliary
 \texttt{l-value($E$)} construct which was expected to evaluate to the l-value of the expression $E$.
 This is only defined when $E$ has an l-value, that is, when $E$ is either a variable or evaluates to
 an array element.  \texttt{l-value($E$)} evaluates to a value of the form \texttt{loc($L$)},
 where $L$ is the location where the value of $E$ can be found; for clarity, we use \texttt{loc}
 to structurally distinguish natural numbers from location values.  In giving semantics to
 \texttt{l-value} there are two cases to consider.  (1) If $E$ is a variable, then all we need
 to do is to grab its location from the environment.  (2) If $E$ is an array element, then we
 first evaluate the array and its index in order to identify the exact location of the element
 of concern, and then return that location; the last rule below works because its preceding
 context declarations ensure that the array and its index are evaluated, and then the rule for
 array lookup (defined above) rewrites the evaluated array access construct to its corresponding
 store lookup operation. 
 \end{latexComment}
 \syntax{\nonTerminal{\sort{Exp}}}{\terminal{l-value(}{\nonTerminal{\sort{K}}}\terminal{)}}{}
 \syntax{\nonTerminal{\sort{Val}}}{\terminal{loc(}{\nonTerminal{\sort{Nat}}}\terminal{)}}{}
 \krule{}{\ensuremath{{\kprefix{green}{k}{\reduce{{\terminal{l-value(}{\variable{X}{Id}}\terminal{)}}}{{\terminal{loc(}{\variable{L}{Nat}}\terminal{)}}}}}\mathrel{\terminal{}}{\kmiddle{violet}{env}{{{\variable{X}{Id}}\mathrel{\terminal{\ensuremath{\mapsto}}}{\variable{L}{Nat}}}}}}}
 \kcontext{}{\ensuremath{\terminal{l-value(}{{{\AnyVar{List\{K\}}}\terminal{[}{{{{{\AnyVar{List\{K\}}}\terminal{,}{\variable{\ensuremath{\square}}{Exp}}}}\terminal{,}{\AnyVar{List\{K\}}}}}\terminal{]}}}\terminal{)}}}
 \kcontext{}{\ensuremath{\terminal{l-value(}{{{\variable{\ensuremath{\square}}{List\{K\}}}\terminal{[}{\AnyVar{List\{K\}}}\terminal{]}}}\terminal{)}}}
 \krule{}{\ensuremath \kprefix{green}{k}{\reduce{{\terminal{l-value(}{{\terminal{lookup(}{\variable{L}{Nat}}\terminal{)}}}\terminal{)}}}{{\terminal{loc(}{\variable{L}{Nat}}\terminal{)}}}}}
 \begin{latexComment}
  \subsection{Length}
 The following operation calculates the length of a list of identifiers.
 We make the two rules structural so they they do not count as computations. 
 \end{latexComment}
 \syntax{\nonTerminal{\sort{Nat}}}{\mid\!\!{\nonTerminal{\sort{List\{Id\}}}}\!\mid}{}
 \kequation{}{\ensuremath \reduceTopS{{\mid\!\!{\constant{\ensuremath{\dotCt{List\{Id\}}}}{List\{Id\}}}\!\mid}}{\constant{0}{Zero}}}
 \kequation{}{\ensuremath \reduceTopS{{\mid\!\!{{{\variable{X}{Id}}\terminal{,}{\variable{Xl}{List\{Id\}}}}}\!\mid}}{{{\constant{1}{Nat}}\mathrel{\terminal{\ensuremath{{}+}\subscript{{\scriptstyle\it{}Nat}}}}{{\mid\!\!{\variable{Xl}{List\{Id\}}}\!\mid}}}}}
 \begin{latexComment}
  \subsection{Sequences of locations}
 The following operation expands to the list of natural numbers between two given numbers.
 The first number is expected to be no larger than the second.
 The two rules below are structural, for the same reason as above. 
 \end{latexComment}
 \syntax{\nonTerminal{\sort{List\{K\}}}}{{\nonTerminal{\sort{Nat}}}\terminal{..}{\nonTerminal{\sort{Nat}}}}{}
 \kequation{}{\ensuremath \reduceTopS{{{\variable{\ensuremath{{N}_{1}}}{Nat}}\terminal{..}{\variable{\ensuremath{{N}_{1}}}{Nat}}}}{\constant{\ensuremath{\dotCt{List\{K\}}}}{List\{KResult\}}}}
 \kcequation{}{\ensuremath \reduceTopS{{{\variable{\ensuremath{{N}_{1}}}{Nat}}\terminal{..}{\variable{\ensuremath{{N}_{2}}}{Nat}}}}{{{\variable{\ensuremath{{N}_{1}}}{Nat}}\mathrel{\terminal{\ensuremath{,\!\!,}}}{{{{{\variable{\ensuremath{{N}_{1}}}{Nat}}\mathrel{\terminal{\ensuremath{{}+}\subscript{{\scriptstyle\it{}Nat}}}}{\constant{1}{Nat}}}}\terminal{..}{\variable{\ensuremath{{N}_{2}}}{Nat}}}}}}}{\ensuremath{{\variable{\ensuremath{{N}_{1}}}{Nat}}\mathrel{\terminal{\ensuremath{{}<}\subscript{{\scriptstyle\it{}Nat}}}}{\variable{\ensuremath{{N}_{2}}}{Nat}}}}
 \begin{latexComment}
  \subsection{Lists of values}
 Currently we have to explicitly declare the syntactic lists
 (they will be eventually builtin).  We need lists of values as a separate syntactic
 category because we want to allow lists of expressions (e.g., function arguments) to
 evaluate to such lists of values.  Note also that we defined lists of values as \K
 results (at the beginning of the SIMPLE semantics module). 
 \end{latexComment}
 \syntax{\nonTerminal{\sort{List\{Val\}}}}{{\nonTerminal{\sort{List\{Val\}}}}\terminal{,}{\nonTerminal{\sort{List\{Val\}}}}}{\kditto{}}
 \syntaxCont{\nonTerminal{\sort{List\{Val\}}}}{\crlbracket{\nonTerminal{\sort{Val}}}}{}
 \syntax{\nonTerminal{\sort{List\{Exp\}}}}{\crlbracket{\nonTerminal{\sort{List\{Val\}}}}}{}
 \end{module}
  The next module puts everything together, namely syntax, semantics and
 programs (note that it includes the SIMPLE semantics, which includes
 the syntax, and the SIMPLE programs). \\
 \begin{module}{\moduleName{SIMPLE-UNTYPED}}
 \including{\moduleName{K}}
 \including{\moduleName{SIMPLE-UNTYPED-PROGRAMS}\modulePlus{}\moduleName{SIMPLE-UNTYPED-SEMANTICS}}
 \syntax{\nonTerminal{\sort{Bag}}}{\terminal{run(}{\nonTerminal{\sort{KLabel}}}\terminal{)}}{}
 \syntaxCont{\nonTerminal{\sort{Bag}}}{\terminal{run(}{\nonTerminal{\sort{KLabel}}}\terminal{,}{\nonTerminal{\sort{List}}}\terminal{)}}{}
 \mequation{}{{\terminal{run(}{\variable{PgmName}{KLabel}}\terminal{)}}}{\kmiddle{red}{T}{\kall{green}{k}{{{{{\variable{PgmName}{KLabel}}\mathrel{\terminal{(}}{\constant{\ensuremath{\dotCt{List\{K\}}}}{List\{KResult\}}}\mathrel{\terminal{)}}}}\mathrel{\terminal{\ensuremath{\kra}}}{\constant{\ensuremath{\terminal{execute}}}{K}}}}}}
 \mequation{}{{\terminal{run(}{\variable{PgmName}{KLabel}}\terminal{,}{\variable{Input}{List}}\terminal{)}}}{\kmiddle{red}{T}{{{\kall{green}{k}{{{{{\variable{PgmName}{KLabel}}\mathrel{\terminal{(}}{\constant{\ensuremath{\dotCt{List\{K\}}}}{List\{KResult\}}}\mathrel{\terminal{)}}}}\mathrel{\terminal{\ensuremath{\kra}}}{\constant{\ensuremath{\terminal{execute}}}{K}}}}}\mathrel{\terminal{}}{\kall{magenta}{in}{\variable{Input}{List}}}}}}
 \begin{latexComment}
  Note that the configurations above use ruptured cells, so they take advantage of
 \K's configuration abstraction mechanism.  They will be automatically completed and
 initialized to match the declared configuration of SIMPLE.  
 \end{latexComment}
 \end{module}